1. References
The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [3] for the third numbered paper by K. L. McMillan):
[1] A. Silburt, A. Evans, G. Vrckovik, M. Diufrensne, and T. Brown, “Functional Verification of ASICs in Silicon Intensive Systems,” presented at DesignCon98 On-Chip System De-sign Conference, 1998.
[2] E. M. Clarke, O. Grumberg, and D. Peled, Model Checking: MIT Press, 1999.
[3] K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem: Kluwer Academic Publishers, 1993.
[4] R. E. Bryant, “Graph-based algorithms for Boolean function manipulation,” IEEE Trans-actions on Computers, vol. C-35(8), pp. 677–691, 1986.
[5] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” in Proceedings of the Design Automation Conference, 1999, pp. 317–320.
[6] P. Bjesse and K. Claessen, “SAT-based verification without state space traversal,” in Proceedings of Conference on Formal Methods in Computer-Aided Design, 2000.
[7] M. Ganai and A. Aziz, “Improved SAT-based Bounded Reachability Analysis,” in Proceedings of VLSI Design Conference, 2002.
[8] P. A. Abdulla, P. Bjesse, and N. Een, “Symbolic Reachability Analysis based on {SAT}-Solvers,” in Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2000.
[9] J. P. Marques-Silva and K. A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, vol. 48, pp. 506–521, 1999.
[10] H. Zhang, “SATO: An efficient propositional prover,” in Proceedings of International Conference on Automated Deduction, vol. 1249, LNAI, 1997, pp. 272–275.
[11] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” in Proceedings of Design Automation Conference, 2001.
[12] M. Ganai, L. Zhang, P. Ashar, and A. Gupta, “Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver,” in Proceedings of the Design Automation Conference, 2002.
[13] A. Kuehlmann, M. Ganai, and V. Paruthi, “Circuit-based Boolean Reasoning,” in Proceedings of Design Automation Conference, 2001.
[14] B. W. Wah, G.-J. Li, and C. F. Yu, “Multiprocessing of Combinational Search Problems,” IEEE computer, pp. 93–108, 1985.
[15] H. Zhang, M. P. Bonacina, and J. Hsiang, “PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems,” Journal of Symbolic Computation, 1996.
[16] Y. Zhao, “Accelerating Boolean Satisfiability through Application Specific Processing.,” Ph.D. Thesis. Princeton, 2001.
[17] C. Powley, C. Fergusion, and R. Korf, “Parallel Heuristic Search: Two Approaches,” in Parallel Algorithms for Machine Intelligence and Vision, V. Kumar, P. S. Gopalakrish-nan, and L. N. Kanal, Eds. New York: Springer-Verlag, 1990.
[18] B. Jurkowiak, C. M. Li, and G. Utard, “Parallelizing Satz Using Dynamic Workload Balancing,” presented at Workshop on Theory and Applications of Satisfiability Testing, 2001.
[19] M. Boehm and E. Speckenmeyer, “A Fast Parallel SAT-solver—Efficient Workload Balancing,” presented at Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Fla., 1994.
[20] U. Stern and D. L. Dill, “Parallelizing the Murphi Verifier,” presented at Computer Aided Verification, 1997.
[21] T. Heyman, D. Geist, O. Grumberg, and A. Schuster, “Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits,” presented at Computer-Aided Verification, 2000.
[22] A. Narayan, A. Isles, J. Jain, R. Brayton, and A. L. Sangiovanni-Vincentelli, “Reachability Analysis using Partitioned-ROBDDs,” presented at International Conference on Computer-Aided Design, 1997.
[23] A. Yadgar, “Parallel SAT Solving for Model Checking. www.cs.technion.ac.il/˜yadgar/Research/research.pdf,” 2002.
[24] M. Davis, G. Longeman, and D. Loveland, “A Machine Program for Theorem Proving,” Communications of the ACM, vol. 5, pp. 394–397, 1962.
[25] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” in Proceedings of Workshop on Tools and Algorithms for Analysis and Construction of Systems (TACAS), vol. 1579, LNCS, 1999.
[26] M. Sheeran, S. Singh, and G. Stalmarck, “Checking Safety Properties using Induction and a SAT Solver,” in Proceedings of Conference on Formal Methods in Computer-Aided Design, 2000.
[27] A. Hasegawa, H. Matsuoka, and K. Nakanishi, “Clustering Software for Linux-Based HPC,” NEC Research & Development, vol. 44, No. 1, pp. 60–63, 2003.
2. Related Work
With increasing design complexity of digital hardware, functional verification has become the most expensive and time-consuming component of the product development cycle according to some practitioners[1]. Verifying modern designs requires robust and scalable approaches in order to meet more-demanding time-to-market requirements. Formal verification techniques like symbolic model checking [2, 3], based on the use of Binary Decision Diagrams (BDDs) [4], offer the potential of exhaustive coverage and the ability to detect subtle bugs in comparison to traditional techniques like simulation. However, these techniques do not scale well in practice due to the state explosion problem.
SAT solvers enjoy several properties that make them attractive as a complement to BDDs. Their performance is less sensitive to the problem sizes and they do not suffer from space explosion. As a result, various researchers have developed routines for performing Bounded Model Checking (BMC) using SAT [5–8]. Unlike symbolic model checking, BMC focuses on finding bugs of a bounded length, and successively increases this bound to search for longer traces. Given a design and a correctness property, BMC techniques generate a Boolean formula, such that the formula is true if and only if there exists a witness/counterexample of length k. This Boolean formula is then checked by a backend SAT solver. Due to the many recent advances in SAT solvers [9–13], SAT-based BMC can handle much larger designs and analyze them faster than before.
A limitation of current applications of BMC is that it can do search up to a maximum depth allowed by the physical memory on a single server. This limitation comes from the fact that, as the search bound k becomes larger, the memory requirement due to unrolling of the design also increases. Especially for the memory-bound designs, a single server with a limited memory has now become a bottleneck to performing deeper search.
Parallelizing SAT solvers has been proposed by many researchers [14–19]. Most of these approaches target performance improvement of the SAT solver. These algorithms are based on partitioning the search space on different processors using partial assignments on the variables. Each processor works on the assigned space and communicates with other processors only after it is done searching its allocated portion of the search space. Such algorithms are not scalable, in terms of memory, due to high data redundancy. This is because, in such an approach each processor keeps the entire problem data (all clauses and variables).
In a closely related work on parallelizing SAT [16], the authors partition the problem by distributing the clauses evenly on many application specific processors. They use fine grain parallelism in the SAT algorithm to get better load balancing and reduce communication costs. Though they target the scalability issue by partitioning the clauses disjointedly, the variables appearing in the clauses are not disjoint. Therefore, whenever a Client finishes Boolean constraint propagation (BCP) on its set of clauses, it must broadcast the newly implied variables to all the other processors. The authors observed that over 90% of messages are broadcast messages. Broadcasting implications can become a serious communication bottleneck when the problem contains millions of variables.
Reducing the space requirement in model checking has been suggested in several related works [20–22]. These studies suggest partitioning the problem in several ways. The work discussed in [20] shows how to parallelize the model checker based on explicit state enumeration. They achieve it by partitioning the state table for reached states into several processing nodes. The work discussed in [21] discusses techniques to parallelize the BDD-based reachability analysis. The state space on which reachability is performed is partitioned into disjoint slices, where each slice is owned by one process. The process executes a reachability algorithm on its own slice. In [22], a single computer is used to handle one task at a time, while the other tasks are kept in external memory. In another paper [23], the author suggested a possibility of distributing SAT-based BMC but has not explored the feasibility of such an approach.
3. Discussions on Some Related Technology
a) State-of-the-art SAT Solver
The Boolean Satisfiability (SAT) problem consists of determining a satisfying assignment for a Boolean formula on the constituent Boolean variables or proving that no such assignment exists. The problem is known to be NP-complete. Most SAT solvers [9–13] employ DPLL style [24] algorithm as shown in FIG. 2.
Three engines of a SAT solver are: decision, deduction, and diagnostic. The decision engine selects a new variable to branch on based on some heuristic. The deduction engine propagates the Boolean constant values on variables through implication (BCP). If a conflict occurs during BCP, the diagnostic engine analyzes the cause of conflict and adds reasons that prevent the same conflict in the future. This often leads to a non-chronological backtrack to some previous decision level which was responsible for the conflict. A Boolean problem can be ex-pressed either in CNF form or logical gate form or both. A hybrid SAT solver as in [12], where the problem is represented as both logical gates and a CNF expression, is well suited for BMC.
b) Bounded Model Checking
In BMC, the specification is expressed in LTL (Linear Temporal Logic), which includes the standard temporal operators—next time operator X, eventuality operator F, globally operator G, and until operator U. The design is described as a standard Kripke structure M=(S, I, T, L), with a finite set of states S, the set of initial states I, a transition relation between states T, and a labeling L of states with atomic propositions.
Given a Kripke structure M, an LTL formula f, and a bound k, the translation task in BMC is to construct a propositional formula [M, f]k, such that the formula is satisfiable if and only if there exists a witness of length k [25]. The formula essentially consists of constraints due to the unrolled transition relation, and constraints due to the property being verified. The satisfiability check is performed by a backend SAT solver. Verification typically proceeds by looking for wit-nesses or counterexamples of increasing length. In practice, a separate argument is needed to determine when to stop, i.e., when a proof is complete [25, 26].
The overall algorithm of a SAT-based BMC for checking a simple safety property is shown in the FIG. 3. Given a bound k and the property node P, the algorithm checks the existence of a witness or counterexample of length less than or equal to k to the property P. The procedure Unroll is invoked at each unroll depth i to do the required unrolling of the circuit. After the unrolling, SAT is invoked to check the satisfiability of the problem on the unrolled circuit. If the SAT check succeeds, it returns WITNESS; else it continues until the bound k is reached, when it returns NO_WITNESS.
The SAT problems generated by the BMC translation procedure grow bigger as k increases. Therefore, the practical efficiency of the backend SAT solver becomes critical in enabling deeper searches to be performed.